Nuprl Lemma : branch_wf
11,40
postcript
pdf
P
:
,
d
:Dec(
P
),
T
:Type,
A
:(
P
T
),
B
:
T
. if
p
:
P
then
A
(
p
) else
B
fi
T
latex
ProofTree
Definitions
Type
,
if
p
:
P
then
A
(
p
) else
B
fi
,
case
b
of inl(
x
) =>
s
(
x
) | inr(
y
) =>
t
(
y
)
,
x
(
s
)
,
f
(
a
)
,
,
x
:
A
.
B
(
x
)
,
False
,
P
Q
,
x
:
A
B
(
x
)
,
Void
,
t
T
,
left
+
right
,
A
,
Dec(
P
)
origin
P:
, d:Dec(P), T:Type, A:(P
T), B:T. if p:P then A(p) else B fi 
T
P:, d:Dec(P), T:Type, A:(PT), B:T. if p:P then A(p) else B fi T
x:A. B(x)
QB(x) T
A